
#ifndef SATTASK_H_
#define SATTASK_H_

#include<string>
#include<fstream>
#include<vector>

using namespace std;

class Clause {
private:
	vector<int> variables;
public:
	Clause() {
	}

	~Clause() {
	}

public:

	void add(int variable) {
		variables.push_back(variable);
	}

	const vector<int>& getVariables() const {
		return variables;
	}

	void print() const {
		for (vector<int>::const_iterator i = variables.begin(); i != variables.end(); i++) {
			cout << *i << " ";
		}
		cout << "\n";
	}
};

class SatTask {
private:
	int variablesNumber;
	vector<Clause> clauses;

public:
	SatTask(ifstream& file) {
		read(file);
	}

	void read(ifstream &file) {
		string str;
		do {
			file >> str;
		} while(str != "cnf");

		int clauses_number;
		file >> variablesNumber >> clauses_number;

		for (int i = 0; i < clauses_number; i++) {
			Clause clause;
			int v = 0;
			while (true) {
				file >> v;
				if (v == 0) {
					break;
				}
				clause.add(v);
			}
			clauses.push_back(clause);
		}
	}

	int const getVariablesNumber() const {
		return variablesNumber;
	}

	~SatTask() {

	}

	void print() const {
		cout << variablesNumber << " " << clauses.size() << "\n";
		for (vector<Clause>::const_iterator i = clauses.begin(); i != clauses.end(); i++) {
			(*i).print();
		}
	}

	const vector<Clause>& getClauses() const {
		return clauses;
	}

	int checkResult(vector<int> result) const {
		for (vector<Clause>::const_iterator i = clauses.begin(); i != clauses.end(); i++) {
			Clause c = *i;
			int bad = true;
			vector<int> variables = c.getVariables();
			for (vector<int>::const_iterator j = variables.begin(); j != variables.end(); j++) {
				if (*j == result[abs(*j) - 1]) {
					bad = false;
					break;
				}
			}
			if (bad) {
				return false;
			}
		}
		return true;
	}

};

#endif /* SATTASK_H_ */
